Apologies for not getting to this sooner, but I have been thinking about your PR. I think everything you've done here is reasonable in terms of the existing API and how the literature is written but I wonder if it makes sense for us to change up how UnboundedOperator is defined to make things smoother for Lean formalization. What doesn't feel quite right to me is

/-- The position operators defined on the Schwartz submodule. -/
def positionOperatorSchwartz : schwartzSubmodule d →ₗ[ℂ] schwartzSubmodule d :=
  (schwartzEquiv (d := d)) ∘ₗ 𝐱[i].toLinearMap ∘ₗ (schwartzEquiv (d := d)).symm

Like I said, why you'd do this makes sense with how things are designed, but needing to use schwartzEquiv to move back and forth between the Schwartz subspace seems like a complication that is going to bite us in the long run. I wonder if it would make more sense to have UnboundedOperator between two different spaces, even if we only intend to use them between the same space because Lean sees the submodule it's defined on as a different space than the entire Hilbert space. So I'm thinking it might be smart to adjust the API before we get too deep.

Unfortunately that would delay this PR but I think it might save some headaches in the long run. Does this reasoning make sense, and do you think this would be a productive change?

@morrison-daniel Could you give your suggested definition for UnboundedOperator here?

I wonder if it would make more sense to have UnboundedOperator between two different spaces, even if we only intend to use them between the same space

I think this change,

structure UnboundedOperator ... extends LinearPMap ℂ HS1 HS2 where ...

could be done relatively easily, but this wouldn't remove the need to map between Schwartz maps and their $$L^2$$ equivalence classes. Maybe I have misunderstood your comment?

You are correct, I realized what I was suggesting wouldn't actually remove what I wanted to remove. I have a tendency to be overly cautious to whether something is being done in the best way which is overkill at this point... Ignore my previous statement I'll review, but it's already looking pretty good!